
; Copyright (c) 2015 Microsoft Corporation
;;segmentation fault instead unsat, 
;; the problem disappears when I relax the constraints by commenting the line 22 : (assert (<= PRICE_SUM 100000))
(set-option :auto-config true)
(declare-fun id_0 () Int)
(declare-fun price_0 () Int)
(declare-fun quality_0 () Int)
(declare-fun end_0 () Int)
(declare-fun begin_0 () Int)
(declare-fun id_1 () Int)
(declare-fun price_1 () Int)
(declare-fun quality_1 () Int)
(declare-fun end_1 () Int)
(declare-fun begin_1 () Int)
(declare-fun id_2 () Int)
(declare-fun price_2 () Int)
(declare-fun quality_2 () Int)
(declare-fun end_2 () Int)
(declare-fun begin_2 () Int)
(assert (or (or (or (or (and (and (and (and (= id_0 0) (= price_0 73)) (= quality_0 123)) (= begin_0 70861964)) (= end_0 167228221)) (and (and (and (and (= id_0 1) (= price_0 1)) (= quality_0 616)) (= begin_0 166528188)) (= end_0 168278516))) (and (and (and (and (= id_0 2) (= price_0 73)) (= quality_0 481)) (= begin_0 68173212)) (= end_0 74650788))) (and (and (and (and (= id_0 3) (= price_0 93)) (= quality_0 99)) (= begin_0 153776232)) (= end_0 170090979))) (and (and (and (and (= id_0 4) (= price_0 103)) (= quality_0 617)) (= begin_0 64739433)) (= end_0 80066843))) )
(assert (or (or (or (or (and (and (and (and (= id_1 5) (= price_1 200)) (= quality_1 28)) (= begin_1 162987111)) (= end_1 173514625)) (and (and (and (and (= id_1 6) (= price_1 699)) (= quality_1 591)) (= begin_1 195333960)) (= end_1 243576121))) (and (and (and (and (= id_1 7) (= price_1 406)) (= quality_1 73)) (= begin_1 171322768)) (= end_1 210353311))) (and (and (and (and (= id_1 8) (= price_1 866)) (= quality_1 74)) (= begin_1 122600344)) (= end_1 181258994))) (and (and (and (and (= id_1 9) (= price_1 555)) (= quality_1 679)) (= begin_1 187974575)) (= end_1 222772145))) )
(assert (or (or (or (or (and (and (and (and (= id_2 10) (= price_2 768)) (= quality_2 280)) (= begin_2 208161023)) (= end_2 216848353)) (and (and (and (and (= id_2 11) (= price_2 933)) (= quality_2 603)) (= begin_2 211683868)) (= end_2 342680230))) (and (and (and (and (= id_2 12) (= price_2 1044)) (= quality_2 849)) (= begin_2 317315222)) (= end_2 324925738))) (and (and (and (and (= id_2 13) (= price_2 989)) (= quality_2 353)) (= begin_2 297798620)) (= end_2 343371249))) (and (and (and (and (= id_2 14) (= price_2 229)) (= quality_2 598)) (= begin_2 295587321)) (= end_2 315183895))) )
(define-fun PRICE_SUM () Int (+ price_0 price_1 price_2))
(assert (<= PRICE_SUM 100000))
(define-fun MAX2 ((a1 Int) (a2 Int)) Int (ite (>= a1 a2) a1 a2))
(define-fun MAX3 ((a1 Int) (a2 Int) (a3 Int) ) Int (MAX2 a1 (MAX2 a2 a3 )))
(define-fun TIME_CRITERIA () Int (MAX3 end_0 end_1 end_2))
(define-fun PLAN_QUALITY () Int TIME_CRITERIA)
(echo "0000")
(check-sat)
(get-value (id_0))
(get-value (id_1))
(get-value (id_2))
(get-value (PLAN_QUALITY))
(get-value (PRICE_SUM))
(assert (< PLAN_QUALITY  315183895))
(echo "11111")
(check-sat)
(get-value (id_0))
(get-value (id_1))
(get-value (id_2))
(get-value (PLAN_QUALITY))
(get-value (PRICE_SUM))
(assert (< PLAN_QUALITY  243576121))
(echo "22222")
(check-sat)
;; (get-value (id_0))
;; (get-value (id_1))
;; (get-value (id_2))
;; (get-value (PLAN_QUALITY))
;; (get-value (PRICE_SUM))
(assert (< PLAN_QUALITY  222772145))
(echo "33333")
(check-sat)
(get-value (id_0))
(get-value (id_1))
(get-value (id_2))
(get-value (PLAN_QUALITY))
(get-value (PRICE_SUM))
(assert (< PLAN_QUALITY  216848353))
(echo "44444")
(check-sat)
(get-value (id_0))
(get-value (id_1))
(get-value (id_2))
(get-value (PLAN_QUALITY))
(get-value (PRICE_SUM))
(echo "The end")
